sig User{
	contacts: set User
}

sig Event{
	creator: one User,
	invited: set User,
	start : one TimeAndDate,
	end: one TimeAndDate,
	weather: one WeatherForecast
}

sig Calendar{
	owner: one User,
	schedule: set Event
}

sig TimeAndDate, WeatherForecast{}

sig WeatherNotification{
	about: one Event,
	sent: set User
}

//FACTS

fact CalendarProperties{
	// one calendar per user
	no disj c1,c2 : Calendar | c2.owner=c1.owner
	//exactly one user per calendar
	#User = #Calendar
}


fact EventProperties{
	//the creator cannot be in participant
	no e: Event | e.creator in e.invited
	//all event must be in the calendar of both the creator and the participant
	all e : Event, c: Calendar | (e in c.schedule)<=>(e.creator=c.owner || c.owner in e.invited)
	//the start date must be different from the end date
	all e: Event | e.start != e.end
	//there's no event where the end date is the start date of another and the stat date is the end date of another
	no e1,e2: Event | (e1.start=e2.end) && (e1.end=e2.start)

}

fact UserProperties{
	//a user cannot be a contact of himself
	no u: User| u in u.contacts
}

fact WeatherNotificationProperties{
	// the notification is sent only to invited+creator
	all wn: WeatherNotification | wn.sent=(wn.about.invited+wn.about.creator)
	// one notification per event
	no disj wn1,wn2: WeatherNotification| wn1.about=wn2.about
}


//ASSERTIONS

assert EventInCalendarConsistency{
	all e: Event, c: Calendar| (e.creator=c.owner ||c.owner in e.invited) implies e in c.schedule 
}

assert NoSelfInviting{
	no e: Event | e.creator in e.invited
}

assert NoSelfContacts{
		no u: User| u in u.contacts	
}

check NoSelfInviting for 5
check NoSelfContacts for 5
check EventInCalendarConsistency for 5


//PREDICATES
	
pred showContacts{}

run showContacts for 0 but exactly 5 User, 5 Calendar

pred showEvents{}

run showEvents for 2 but exactly 2 User, exactly 5 Event, 0 WeatherNotification


pred show {}


run show for 5








